\begin{tabbing}
$\forall$$T$:Type, $L$:$T$ List, $P$:($T$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$T$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ (\=$\exists$$L_{1}$, $L_{2}$:$T$ List.\+
\\[0ex]interleaving($T$;$L_{1}$;$L_{2}$;$L$)
\\[0ex]\& ($\forall$$x$:$T$. ($x$ $\in$ $L_{1}$) $\Leftrightarrow$ ($x$ $\in$ $L$) \& $P$($x$))
\\[0ex]\& ($\forall$$x$:$T$. ($x$ $\in$ $L_{2}$) $\Leftrightarrow$ ($x$ $\in$ $L$) \& $\neg$$P$($x$)))
\-
\end{tabbing}